Quiz 9 (Week 9)

1.1 Recognizing phantom types

1.1.1 Question 1

Consider the following type definitions.

data Day we
  = Mon | Tue | Wed | Thu | Fri
  | Sat we | Sun we

data Free
data Taken
data Locker state = Locker (Maybe Int)

data List1 a b = List1 [b]
data List2 a b = Nil | List2 b (List2 a b)

Which of the types above are phantom types?

1.2 Safe Division

We can use phantom types to avoid divide-by-zero errors as follows:

data Zero
data NonZero
data CheckedInt t = Checked Int

safeDiv :: Int -> CheckedInt NonZero -> Int
safeDiv x (Checked y) = x `div` y

1.2.1 Question 2

Which of the following statements are true?

The type argument t does not occur in Checked.
The types Zero and NonZero are both phantom types.
This code will not compile as Zero and NonZero have not been defined.
The pattern matching in safeDiv is non-exhaustive (i.e. missing cases).

1.2.2 Question 3

Which of the following could be a valid type signature for a function add that calculates the sum of any two CheckedInt values?

CheckedInt NonZero -> CheckedInt NonZero -> CheckedInt NonZero
CheckedInt a -> CheckedInt a -> CheckedInt a
CheckedInt a -> CheckedInt b -> Int
CheckedInt a -> CheckedInt b -> CheckedInt c

1.2.3 Question 4

Choose the best type to give to a smart constructor for the type CheckedInt!

check :: Int -> CheckedInt NonZero
check :: Int -> CheckedInt (Either Zero NonZero)
check :: Int -> CheckedInt t
check :: Int -> Either (CheckedInt Zero) (CheckedInt NonZero)

1.3 Data Kinds

Here we use phantom types with an argument of kind Size to make vectors of various dimensions. Note that the vector size is not statically checked by the default V data constructor. We must be sure to only use the given smart constructors that establish the length invariant about the data:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Size = OneD  | TwoD | ThreeD
newtype Vector (s :: Size) a = V [a]

vec1D :: a -> Vector OneD a
vec1D a = V [a]

vec2D :: (a, a) -> Vector TwoD a
vec2D (a,b) = V [a,b]

vec3D :: (a, a, a) -> Vector ThreeD a
vec3D (a,b,c) = V [a,b,c]

1.3.1 Question 5

Which of the following implementations of vector addition ensure via a static check that the precondition that the vectors must be the same size (and only that precondition), as well as the postcondition that the output vector will be the same size as the input?

addV :: (Num n) => Vector a n -> Vector b n -> Vector c n
addV (V xs) (V ys) = V (zipWith (+) xs ys)

addV :: (Num n) => Vector a n -> Vector a n -> Vector a n
addV (V xs) (V ys) = V (zipWith (+) xs ys)

addV :: (Num n) => Vector TwoD n -> Vector TwoD n -> Vector TwoD n
addV (V xs) (V ys) = V (zipWith (+) xs ys)

addV :: (Num n) => Vector a n -> Vector a n -> Vector b n
addV (V xs) (V ys) = V (zipWith (+) xs ys)

1.3.2 Question 6

Suppose we made a Matrix type using vectors of vectors:

type Matrix r c a = Vector r (Vector c a)

What would be a correct type for a matrix multiplication function?

mm :: Num a => Matrix r i a -> Matrix r i a -> Matrix r i a
mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r i a
mm :: Num a => Matrix r i a -> Matrix c i a -> Matrix i i a
mm :: Num a => Matrix r i a -> Matrix i c a -> Matrix r c a

1.4 Static Assurance

1.4.1 Question 7

Select all true statements below.

Testing is the most common form of static analysis.
You can compile and run your Haskell program even if it fails type checking.
Types and model checkers are forms of static assurance.
Static means of assurance can analyze programs without running them.

1.4.2 Question 8

Which of the following is ruled out by Rice's theorem?

Deciding whether a program contains a while loop.
Deciding whether a computable function always returns non-zero output.
Deciding whether a Haskell program has type Int -> Int.
Deciding whether a Haskell program has type Int -> CheckedInt NonZero.